;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
; Interface for the rotate module, which
; is the module responsible for rotating
; images either 90, 180, or 270 degrees.
(interface IRotate
  
  (sig rotate (tree angle))
  (sig rotate-90 (tree))
  (sig rotate-90-helper (oldtr oldwidth newtr xcurr xmax ycurr ymax currrow))
  (sig rotate-180 (tree))
  (sig rotate-180-helper (oldtr height newtr xcurr xmax ycurr ymax currow))
  (sig rotate-270 (tree))
  (sig rotate-270-helper (oldtr newtr xcurr xmax ycurr ymax currow))
  
  ; verifies that rotate returns a tree
  (con rotate-returns-tree
       (implies (and (tree? tr) 
                     (or (= angle 90) (= angle 180) (= angle 270))))
       (tree? (rotate tr angle)))
  
  ; verifies that rotate-90 returns a tree
  (con rotate-90-returns-tree
       (implies (tree? tr))
       (tree? (rotate-90 tr)))
  
  ; verifies that rotate-180 returns a tree
  (con rotate-180-returns-tree
       (implies (tree? tr))
       (tree? (rotate-180 tr)))
  
  ; verifies that rotate-270 returns a tree
  (con rotate-270-returns-tree
       (implies (tree? tr))
       (tree? (rotate-270 tr)))
  
  ; verifies that rotate-90-helper returns a tree
  (con rotate-90-helper-returns-tree
       (implies (and (tree? oldtr) (natp oldwidth) (tree? newtr) (= xcurr 0) 
                     (= ycurr 0) (natp xmax) (natp ymax)))
       (tree? (rotate-90-helper oldtr oldwidth newtr xcurr xmax ycurr ymax)))
  
  ; verifies that rotate-180-helper returns a tree
  (con rotate-180-helper-returns-tree
       (implies (and (tree? oldtr) (natp height) (tree? newtr) (= xcurr 0) 
                     (= ycurr 0) (natp xmax) (natp ymax)))
       (tree? (rotate-180-helper oldtr height newtr xcurr xmax ycurr ymax)))
  
  ; verifies that rotate-270-helper returns a tree
  (con rotate-270-helper-returns-tree
       (implies (and (tree? oldtr) (tree? newtr) (= xcurr 0) 
                     (= ycurr 0) (natp xmax) (natp ymax)))
       (tree? (rotate-270-helper oldtr newtr xcurr xmax ycurr ymax))))